state ds
k:A sends [tg, e.f(e):B] on l
== (e:E. kind(e) = rcv(l,tg)  valtype(e)  B)
== & (x:Id. vartype(source(l);x)  ds(x)?Top)
== & (e:E. kind(e) = k  loc(e) = source(l)  valtype(e)  A)
== & e@source(l). kind(e) = k  isl(f(e))  (e':E. kind(e') = rcv(l,tg) & sender(e') = e)
== & & (e':E.
== & & (kind(e') = rcv(l,tg)
== & & ( kind(sender(e')) = k & isl(f(sender(e'))) & val(e') = outl(f(sender(e'))))
== & & (e':E.
== & & (kind(e') = rcv(l,tg)
== & & ( (e'':E. kind(e'') = rcv(l,tg)  sender(e'') = sender(e')  e'' = e')) 

latex

---

clarification:

es-kind-sends-iff(es;k;A;l;tg;B;ds;e.f(e))
== (e:es-E(es). es-kind(es; e) = rcv(l,tg)  Knd  es-valtype(es; e)  B)
== & (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & (e:es-E(es).
== & (es-kind(es; e) = k  Knd  es-loc(es; e) = source(l)  Id  es-valtype(es; e)  A)
== & alle-at(es;source(l);e.es-kind(es; e) = k  Knd
== & alle-at(es;source(l);e. isl(f(e))
== & alle-at(es;source(l);e. (e':es-E(es).
== & alle-at(es;source(l);e. (es-kind(es; e') = rcv(l,tg)  Knd
== & alle-at(es;source(l);e. (& es-sender(es; e') = e  es-E(es)))
== & & (e':es-E(es).
== & & (es-kind(es; e') = rcv(l,tg)  Knd
== & & ( es-kind(es; es-sender(es; e')) = k  Knd
== & & ( & isl(f(es-sender(es; e')))
== & & ( & es-val(es; e') = outl(f(es-sender(es; e')))  B)
== & & (e':es-E(es).
== & & (es-kind(es; e') = rcv(l,tg)  Knd
== & & ( (e'':es-E(es).
== & & ( (es-kind(es; e'') = rcv(l,tg)  Knd
== & & ( ( es-sender(es; e'') = es-sender(es; e')  es-E(es)
== & & ( ( e'' = e'  es-E(es))) 

latex

Definitions	vartype(i;x), f(x)?z, IdDeq, Top, Id, loc(e), valtype(e), e@i. P(e), source(l), x:A. B(x), P & Q, A & B, b, isl(x), val(e), outl(x), x:A. B(x), Knd, kind(e), rcv(l,tg), P  Q, sender(e), s = t, E
FDL editor aliases	es-kind-sends-iff